
%% bare_jrnl.tex
%% V1.3
%% 2007/01/11
%% by Michael Shell
%% see http://www.michaelshell.org/
%% for current contact information.
%%
%% This is a skeleton file demonstrating the use of IEEEtran.cls
%% (requires IEEEtran.cls version 1.7 or later) with an IEEE journal paper.
%%
%% Support sites:
%% http://www.michaelshell.org/tex/ieeetran/
%% http://www.ctan.org/tex-archive/macros/latex/contrib/IEEEtran/
%% and
%% http://www.ieee.org/



% *** Authors should verify (and, if needed, correct) their LaTeX system  ***
% *** with the testflow diagnostic prior to trusting their LaTeX platform ***
% *** with production work. IEEE's font choices can trigger bugs that do  ***
% *** not appear when using other class files.                            ***
% The testflow support page is at:
% http://www.michaelshell.org/tex/testflow/


%%*************************************************************************
%% Legal Notice:
%% This code is offered as-is without any warranty either expressed or
%% implied; without even the implied warranty of MERCHANTABILITY or
%% FITNESS FOR A PARTICULAR PURPOSE!
%% User assumes all risk.
%% In no event shall IEEE or any contributor to this code be liable for
%% any damages or losses, including, but not limited to, incidental,
%% consequential, or any other damages, resulting from the use or misuse
%% of any information contained here.
%%
%% All comments are the opinions of their respective authors and are not
%% necessarily endorsed by the IEEE.
%%
%% This work is distributed under the LaTeX Project Public License (LPPL)
%% ( http://www.latex-project.org/ ) version 1.3, and may be freely used,
%% distributed and modified. A copy of the LPPL, version 1.3, is included
%% in the base LaTeX documentation of all distributions of LaTeX released
%% 2003/12/01 or later.
%% Retain all contribution notices and credits.
%% ** Modified files should be clearly indicated as such, including  **
%% ** renaming them and changing author support contact information. **
%%
%% File list of work: IEEEtran.cls, IEEEtran_HOWTO.pdf, bare_adv.tex,
%%                    bare_conf.tex, bare_jrnl.tex, bare_jrnl_compsoc.tex
%%*************************************************************************

% Note that the a4paper option is mainly intended so that authors in
% countries using A4 can easily print to A4 and see how their papers will
% look in print - the typesetting of the document will not typically be
% affected with changes in paper size (but the bottom and side margins will).
% Use the testflow package mentioned above to verify correct handling of
% both paper sizes by the user's LaTeX system.
%
% Also note that the "draftcls" or "draftclsnofoot", not "draft", option
% should be used if it is desired that the figures are to be displayed in
% draft mode.
%
\documentclass[journal]{IEEEtran}
%
% If IEEEtran.cls has not been installed into the LaTeX system files,
% manually specify the path to it like:
% \documentclass[journal]{../sty/IEEEtran}





% Some very useful LaTeX packages include:
% (uncomment the ones you want to load)


% *** MISC UTILITY PACKAGES ***
%
%\usepackage{ifpdf}
% Heiko Oberdiek's ifpdf.sty is very useful if you need conditional
% compilation based on whether the output is pdf or dvi.
% usage:
% \ifpdf
%   % pdf code
% \else
%   % dvi code
% \fi
% The latest version of ifpdf.sty can be obtained from:
% http://www.ctan.org/tex-archive/macros/latex/contrib/oberdiek/
% Also, note that IEEEtran.cls V1.7 and later provides a builtin
% \ifCLASSINFOpdf conditional that works the same way.
% When switching from latex to pdflatex and vice-versa, the compiler may
% have to be run twice to clear warning/error messages.






% *** CITATION PACKAGES ***
%
%\usepackage{cite}
% cite.sty was written by Donald Arseneau
% V1.6 and later of IEEEtran pre-defines the format of the cite.sty package
% \cite{} output to follow that of IEEE. Loading the cite package will
% result in citation numbers being automatically sorted and properly
% "compressed/ranged". e.g., [1], [9], [2], [7], [5], [6] without using
% cite.sty will become [1], [2], [5]--[7], [9] using cite.sty. cite.sty's
% \cite will automatically add leading space, if needed. Use cite.sty's
% noadjust option (cite.sty V3.8 and later) if you want to turn this off.
% cite.sty is already installed on most LaTeX systems. Be sure and use
% version 4.0 (2003-05-27) and later if using hyperref.sty. cite.sty does
% not currently provide for hyperlinked citations.
% The latest version can be obtained at:
% http://www.ctan.org/tex-archive/macros/latex/contrib/cite/
% The documentation is contained in the cite.sty file itself.






% *** GRAPHICS RELATED PACKAGES ***
%
\ifCLASSINFOpdf
 \usepackage[pdftex]{graphicx}
  % declare the path(s) where your graphic files are
  % \graphicspath{{../pdf/}{../jpeg/}}
  % and their extensions so you won't have to specify these with
  % every instance of \includegraphics
  % \DeclareGraphicsExtensions{.pdf,.jpeg,.png}
\else
  % or other class option (dvipsone, dvipdf, if not using dvips). graphicx
  % will default to the driver specified in the system graphics.cfg if no
  % driver is specified.
   \usepackage[dvips]{graphicx}
  % declare the path(s) where your graphic files are
  % \graphicspath{{../eps/}}
  % and their extensions so you won't have to specify these with
  % every instance of \includegraphics
  % \DeclareGraphicsExtensions{.eps}
\fi
% graphicx was written by David Carlisle and Sebastian Rahtz. It is
% required if you want graphics, photos, etc. graphicx.sty is already
% installed on most LaTeX systems. The latest version and documentation can
% be obtained at:
% http://www.ctan.org/tex-archive/macros/latex/required/graphics/
% Another good source of documentation is "Using Imported Graphics in
% LaTeX2e" by Keith Reckdahl which can be found as epslatex.ps or
% epslatex.pdf at: http://www.ctan.org/tex-archive/info/
%
% latex, and pdflatex in dvi mode, support graphics in encapsulated
% postscript (.eps) format. pdflatex in pdf mode supports graphics
% in .pdf, .jpeg, .png and .mps (metapost) formats. Users should ensure
% that all non-photo figures use a vector format (.eps, .pdf, .mps) and
% not a bitmapped formats (.jpeg, .png). IEEE frowns on bitmapped formats
% which can result in "jaggedy"/blurry rendering of lines and letters as
% well as large increases in file sizes.
%
% You can find documentation about the pdfTeX application at:
% http://www.tug.org/applications/pdftex





% *** MATH PACKAGES ***
%
%\usepackage[cmex10]{amsmath}
% A popular package from the American Mathematical Society that provides
% many useful and powerful commands for dealing with mathematics. If using
% it, be sure to load this package with the cmex10 option to ensure that
% only type 1 fonts will utilized at all point sizes. Without this option,
% it is possible that some math symbols, particularly those within
% footnotes, will be rendered in bitmap form which will result in a
% document that can not be IEEE Xplore compliant!
%
% Also, note that the amsmath package sets \interdisplaylinepenalty to 10000
% thus preventing page breaks from occurring within multiline equations. Use:
%\interdisplaylinepenalty=2500
% after loading amsmath to restore such page breaks as IEEEtran.cls normally
% does. amsmath.sty is already installed on most LaTeX systems. The latest
% version and documentation can be obtained at:
% http://www.ctan.org/tex-archive/macros/latex/required/amslatex/math/





% *** SPECIALIZED LIST PACKAGES ***
%
%\usepackage{algorithmic}
% algorithmic.sty was written by Peter Williams and Rogerio Brito.
% This package provides an algorithmic environment fo describing algorithms.
% You can use the algorithmic environment in-text or within a figure
% environment to provide for a floating algorithm. Do NOT use the algorithm
% floating environment provided by algorithm.sty (by the same authors) or
% algorithm2e.sty (by Christophe Fiorio) as IEEE does not use dedicated
% algorithm float types and packages that provide these will not provide
% correct IEEE style captions. The latest version and documentation of
% algorithmic.sty can be obtained at:
% http://www.ctan.org/tex-archive/macros/latex/contrib/algorithms/
% There is also a support site at:
% http://algorithms.berlios.de/index.html
% Also of interest may be the (relatively newer and more customizable)
% algorithmicx.sty package by Szasz Janos:
% http://www.ctan.org/tex-archive/macros/latex/contrib/algorithmicx/




% *** ALIGNMENT PACKAGES ***
%
%\usepackage{array}
% Frank Mittelbach's and David Carlisle's array.sty patches and improves
% the standard LaTeX2e array and tabular environments to provide better
% appearance and additional user controls. As the default LaTeX2e table
% generation code is lacking to the point of almost being broken with
% respect to the quality of the end results, all users are strongly
% advised to use an enhanced (at the very least that provided by array.sty)
% set of table tools. array.sty is already installed on most systems. The
% latest version and documentation can be obtained at:
% http://www.ctan.org/tex-archive/macros/latex/required/tools/


%\usepackage{mdwmath}
%\usepackage{mdwtab}
% Also highly recommended is Mark Wooding's extremely powerful MDW tools,
% especially mdwmath.sty and mdwtab.sty which are used to format equations
% and tables, respectively. The MDWtools set is already installed on most
% LaTeX systems. The lastest version and documentation is available at:
% http://www.ctan.org/tex-archive/macros/latex/contrib/mdwtools/


% IEEEtran contains the IEEEeqnarray family of commands that can be used to
% generate multiline equations as well as matrices, tables, etc., of high
% quality.


%\usepackage{eqparbox}
% Also of notable interest is Scott Pakin's eqparbox package for creating
% (automatically sized) equal width boxes - aka "natural width parboxes".
% Available at:
% http://www.ctan.org/tex-archive/macros/latex/contrib/eqparbox/





% *** SUBFIGURE PACKAGES ***
%\usepackage[tight,footnotesize]{subfigure}
% subfigure.sty was written by Steven Douglas Cochran. This package makes it
% easy to put subfigures in your figures. e.g., "Figure 1a and 1b". For IEEE
% work, it is a good idea to load it with the tight package option to reduce
% the amount of white space around the subfigures. subfigure.sty is already
% installed on most LaTeX systems. The latest version and documentation can
% be obtained at:
% http://www.ctan.org/tex-archive/obsolete/macros/latex/contrib/subfigure/
% subfigure.sty has been superceeded by subfig.sty.



%\usepackage[caption=false]{caption}
%\usepackage[font=footnotesize]{subfig}
% subfig.sty, also written by Steven Douglas Cochran, is the modern
% replacement for subfigure.sty. However, subfig.sty requires and
% automatically loads Axel Sommerfeldt's caption.sty which will override
% IEEEtran.cls handling of captions and this will result in nonIEEE style
% figure/table captions. To prevent this problem, be sure and preload
% caption.sty with its "caption=false" package option. This is will preserve
% IEEEtran.cls handing of captions. Version 1.3 (2005/06/28) and later
% (recommended due to many improvements over 1.2) of subfig.sty supports
% the caption=false option directly:
%\usepackage[caption=false,font=footnotesize]{subfig}
%
% The latest version and documentation can be obtained at:
% http://www.ctan.org/tex-archive/macros/latex/contrib/subfig/
% The latest version and documentation of caption.sty can be obtained at:
% http://www.ctan.org/tex-archive/macros/latex/contrib/caption/




% *** FLOAT PACKAGES ***
%
%\usepackage{fixltx2e}
% fixltx2e, the successor to the earlier fix2col.sty, was written by
% Frank Mittelbach and David Carlisle. This package corrects a few problems
% in the LaTeX2e kernel, the most notable of which is that in current
% LaTeX2e releases, the ordering of single and double column floats is not
% guaranteed to be preserved. Thus, an unpatched LaTeX2e can allow a
% single column figure to be placed prior to an earlier double column
% figure. The latest version and documentation can be found at:
% http://www.ctan.org/tex-archive/macros/latex/base/



%\usepackage{stfloats}
% stfloats.sty was written by Sigitas Tolusis. This package gives LaTeX2e
% the ability to do double column floats at the bottom of the page as well
% as the top. (e.g., "\begin{figure*}[!b]" is not normally possible in
% LaTeX2e). It also provides a command:
%\fnbelowfloat
% to enable the placement of footnotes below bottom floats (the standard
% LaTeX2e kernel puts them above bottom floats). This is an invasive package
% which rewrites many portions of the LaTeX2e float routines. It may not work
% with other packages that modify the LaTeX2e float routines. The latest
% version and documentation can be obtained at:
% http://www.ctan.org/tex-archive/macros/latex/contrib/sttools/
% Documentation is contained in the stfloats.sty comments as well as in the
% presfull.pdf file. Do not use the stfloats baselinefloat ability as IEEE
% does not allow \baselineskip to stretch. Authors submitting work to the
% IEEE should note that IEEE rarely uses double column equations and
% that authors should try to avoid such use. Do not be tempted to use the
% cuted.sty or midfloat.sty packages (also by Sigitas Tolusis) as IEEE does
% not format its papers in such ways.


%\ifCLASSOPTIONcaptionsoff
%  \usepackage[nomarkers]{endfloat}
% \let\MYoriglatexcaption\caption
% \renewcommand{\caption}[2][\relax]{\MYoriglatexcaption[#2]{#2}}
%\fi
% endfloat.sty was written by James Darrell McCauley and Jeff Goldberg.
% This package may be useful when used in conjunction with IEEEtran.cls'
% captionsoff option. Some IEEE journals/societies require that submissions
% have lists of figures/tables at the end of the paper and that
% figures/tables without any captions are placed on a page by themselves at
% the end of the document. If needed, the draftcls IEEEtran class option or
% \CLASSINPUTbaselinestretch interface can be used to increase the line
% spacing as well. Be sure and use the nomarkers option of endfloat to
% prevent endfloat from "marking" where the figures would have been placed
% in the text. The two hack lines of code above are a slight modification of
% that suggested by in the endfloat docs (section 8.3.1) to ensure that
% the full captions always appear in the list of figures/tables - even if
% the user used the short optional argument of \caption[]{}.
% IEEE papers do not typically make use of \caption[]'s optional argument,
% so this should not be an issue. A similar trick can be used to disable
% captions of packages such as subfig.sty that lack options to turn off
% the subcaptions:
% For subfig.sty:
% \let\MYorigsubfloat\subfloat
% \renewcommand{\subfloat}[2][\relax]{\MYorigsubfloat[]{#2}}
% For subfigure.sty:
% \let\MYorigsubfigure\subfigure
% \renewcommand{\subfigure}[2][\relax]{\MYorigsubfigure[]{#2}}
% However, the above trick will not work if both optional arguments of
% the \subfloat/subfig command are used. Furthermore, there needs to be a
% description of each subfigure *somewhere* and endfloat does not add
% subfigure captions to its list of figures. Thus, the best approach is to
% avoid the use of subfigure captions (many IEEE journals avoid them anyway)
% and instead reference/explain all the subfigures within the main caption.
% The latest version of endfloat.sty and its documentation can obtained at:
% http://www.ctan.org/tex-archive/macros/latex/contrib/endfloat/
%
% The IEEEtran \ifCLASSOPTIONcaptionsoff conditional can also be used
% later in the document, say, to conditionally put the References on a
% page by themselves.





% *** PDF, URL AND HYPERLINK PACKAGES ***
%
%\usepackage{url}
% url.sty was written by Donald Arseneau. It provides better support for
% handling and breaking URLs. url.sty is already installed on most LaTeX
% systems. The latest version can be obtained at:
% http://www.ctan.org/tex-archive/macros/latex/contrib/misc/
% Read the url.sty source comments for usage information. Basically,
% \url{my_url_here}.





% *** Do not adjust lengths that control margins, column widths, etc. ***
% *** Do not use packages that alter fonts (such as pslatex).         ***
% There should be no need to do such things with IEEEtran.cls V1.6 and later.
% (Unless specifically asked to do so by the journal or conference you plan
% to submit to, of course. )


% correct bad hyphenation here
\hyphenation{op-tical net-works semi-conduc-tor}


\begin{document}
%
% paper title
% can use linebreaks \\ within to get better formatting as desired
\title{Formalization and Verification of PLC Timers in Coq}
%
%
% author names and IEEE memberships
% note positions of commas and nonbreaking spaces ( ~ ) LaTeX will not break
% a structure at a ~ so this keeps an author's name from being broken across
% two lines.
% use \thanks{} to gain access to the first footnote area
% a separate \thanks must be used for each paragraph as LaTeX2e's \thanks
% was not built to handle multiple paragraphs
%

\author{Hai~Wan, Gang~Chen, Xiaoyu~Song, Ming~Gu% <-this % stops a space
}

% note the % following the last \IEEEmembership and also \thanks -
% these prevent an unwanted space from occurring between the last author name
% and the end of the author line. i.e., if you had this:
%
% \author{....lastname \thanks{...} \thanks{...} }
%                     ^------------^------------^----Do not want these spaces!
%
% a space would be appended to the last name and could cause every name on that
% line to be shifted left slightly. This is one of those "LaTeX things". For
% instance, "\textbf{A} \textbf{B}" will typeset as "A B" not "AB". To get
% "AB" then you have to do: "\textbf{A}\textbf{B}"
% \thanks is no different in this regard, so shield the last } of each \thanks
% that ends a line with a % and do not let a space in before the next \thanks.
% Spaces after \IEEEmembership other than the last one are OK (and needed) as
% you are supposed to have spaces between the names. For what it is worth,
% this is a minor point as most people would not even notice if the said evil
% space somehow managed to creep in.



% The paper headers
\markboth{}%
{}
% The only time the second header will appear is for the odd numbered pages
% after the title page when using the twoside option.
%
% *** Note that you probably will NOT want to include the author's ***
% *** name in the headers of peer review papers.                   ***
% You can use \ifCLASSOPTIONpeerreview for conditional compilation here if
% you desire.




% If you want to put a publisher's ID mark on the page you can do it like
% this:
%\IEEEpubid{0000--0000/00\$00.00~\copyright~2007 IEEE}
% Remember, if you use this you must call \IEEEpubidadjcol in the second
% column for its text to clear the IEEEpubid mark.



% use for special paper notices
%\IEEEspecialpapernotice{(Invited Paper)}




% make the title area
\maketitle


\begin{abstract}
%\boldmath
Programmable logic controllers (PLCs) are widely used in embedded systems. A timer plays a pivotal
role in PLC real-time applications. The paper presents a formalization of TON-timers of PLC
programs in the theorem proving system Coq. The behavior of a timer is characterized by a set of
axioms at an abstract level. PLC programs with timers are modeled in Coq. As a case study, the quiz
machine problem with timer is investigated. Relevant timing properties of practical interests are
proposed and proven in Coq. This work unveils the hardness of timer modeling in embedded systems.
It is a first attempt of formally proving the correctness of PLC programs with timer control.
\end{abstract}
% IEEEtran.cls defaults to using nonbold math in the Abstract.
% This preserves the distinction between vectors and scalars. However,
% if the journal you are submitting to favors bold math in the abstract,
% then you can use LaTeX's standard command \boldmath at the very start
% of the abstract to achieve this. Many IEEE journals frown on math
% in the abstract anyway.

% Note that keywords are not normally used for peerreview papers.
\begin{IEEEkeywords}
PLC, real-time systems, theorem proving, Coq, TON-timer.
\end{IEEEkeywords}






% For peer review papers, you can put extra information on the cover
% page as needed:
% \ifCLASSOPTIONpeerreview
% \begin{center} \bfseries EDICS Category: 3-BBND \end{center}
% \fi
%
% For peerreview papers, this IEEEtran command inserts a page break and
% creates the second title. It will be ignored for other modes.
\IEEEpeerreviewmaketitle


\section{Introduction}

Programmable logic controllers (PLCs) are widely used for safety critical applications in various
industrial fields. The correctness and reliability of PLC programs are of great importance. The use
of timers is one of the distinguished features of PLCs programs. The main focus of this paper is
the modeling and verification of PLC programs with timers.

Based on the operational semantics, in \cite{Mader99timedautomaton} PLC programs are translated
into timed automata. They proposed two ways to model timers: one is to treat timers as symbolic
function block calls and the other is to model timers as separate timed automata. Model checker
UPPAAL is employed to verify the model. In
\cite{ProvingSequentialFunctionChartProgramsUsingAutomata}, timed automata are used to model
Sequential Function Chart programs. In their work, the use of timers is restricted -- each step is
associated with a timer and the timer is taken for guarding the transitions -- in other words, they
did not model timers in their most general forms. A special automata that orients real-time systems
-- PLC-automaton is developed to model the specifications of real-time applications. Structured
Text programs can be automatically generated from PLC-automata\cite{dierks01plcautomata}. They did
not model PLC programs with timers, but use timers to implement PLC-automata. In
\cite{NBauer:Thesis:1998} condition/event systems are adopted to model PLC programs. There is an
assumption that timers can be started only at the beginning of the calculation phase. In
\cite{ModellingPLCLV}, the Ladder Diagram programs are investigated and time is treated implicitly.
Model checker SMV was used to verify the model. The methods mentioned above are all related to the
model checking technologies.

Besides model checking, theorem proving is also employed in verification of PLC Programs. In
\cite{DBLP:journals/rts/KramerV97} theorem prover Isabelle/HOL system was used to model and verify
PLC programs. Modular verification method is adopted in the paper. They had a simple model of time,
because they assumed the the current value increases monotonously and there is no reset action
during this process. No explicit model of a timer was given. In \cite{SynSignalModelPLC}, the
synchronous language SIGNAL is used to model Structured Text and Function Block Diagram programs.
They did not treat timer instructions.

This paper is an attempt of formally proving the correctness of PLC programs with timer control.
The Coq theorem prover is chosen as our formal verification tool. It allows  problem specification,
program formalization and property proving in a single working environment. A timed quiz machine
problem is employed as the case study example.

Informally, the main properties under investigation are statements of the forms that, if a proper
sequence of stimuli are received by the PLC program, then some expected outcomes will be observed.
The problem becomes involved as the timer input depends on its output in previous cycle. By the
nature of the TON timer, its input signals have to be kept stable during the timing period. That
is, their values have to be constant between the start of timing process and the timeout point.
However, the cyclic program structure does not make this property obvious. To make the proving
process manageable without loss of generality, we will introduce three abstract axioms at an
appropriate level to characterize the behavior of TON timer (see section \ref{model_timer} for
details).

As the first step in this formalization, we assume the existence of a function $f$ which maps the
start of each scan cycle to its time point. This function is abstract and it needs only to satisfy
a monotonic requirement. Such an assumption allows us to establish the relation between scan cycles
(see next section for the descriptions of PLC and the notion of scan cycle) and real time points
without explicitly calculating the exact time period of each cycle. It should be noted that the
adoption of this function relies on the programming practice that the timer output is sampled only
once in the program. A subtle issue in this formal model is the selection of the starting and
ending points of each scan cycle. In the PLC convention, a scan cycle starts with the input phase,
followed by the execution phase and the output phase. As a result, the definition of the function
$f$ encounters many choices. It can map the start of the input phase to time, or map the start of
the execution phase or the start of the output phase to time. Such a selection would give different
interpretations to timer axioms and will influence the forms of system properties. A further
discussion on this issue can be found in section \ref{assumption_constraits} and \ref{model_time}.

With the preparation given above, we can give an informal description on the axiomatic assumptions
of TON timer:

\begin{itemize}

\item if the main input to the timer turns off, so does the timeout signal;

\item if the preset timeout  period is  passed and that the main timer
input has been kept ON during this period, then the timeout signal will turn on (or keep on) at
next cycle;

\item if the timeout signal will be turned on at next cycle, then the
main input signal must have been kept on for a period larger than the preset timing period.

\end{itemize}

The precise description of these hypothesis is presented in section \ref{interpretation_loc}. These
assumptions characterize the global behavior of TON timer. They appear both reasonable and
sufficient for the verification of most timer-related problems.

From this study, it made clear that formal PLC verification can benefit from Coq in many aspects.
First, Coq gives us enough expressive power to model PLC programs with timers at any desired
abstract level. A formal timer model, expressed in a set of Coq axioms or hypothesis, can abstract
away the differences among timers with different resolutions. The abstraction facilitates the
modeling and verification process. Second, Coq allows us to prove parameterized properties, which
is a useful feature not directly supported by model checking. Third, it is easy to model objects by
parameterized Coq modules so that specifications and proofs can be reused and scalable.

The rest of the paper is organized as follows. In the following section, we give a short
introduction to PLC and its timers. A quiz machine example is described in Section \ref{example}.
The example is employed throughout the paper. In Section \ref{model_timer}, we describe the method
of modeling timers in the theorem prover Coq in detail. Section \ref{whold_model} shows the
complete model of the example program and outlines the proof. Finally, Section \ref{conclusion}
concludes the paper.

\section{Programmable Logic Controller and Timers}

%\begin{figure}[]
%        \center\includegraphics[scale = 0.5]
%        {figs/structure_plc}
%        \caption{\label{structure_plc} PLC cycle}
%      \end{figure}

A PLC system typically consists of a CPU, a memory and input/output points through which the system
communicates with its outside environment. The execution of a PLC program is an infinite loop in
which each iteration is called scan cycle. Typically, each scan cycle can be divided into three
phases:

\begin{enumerate}

\item \textbf{Input phase} during which PLC system
reads the values of sensors and copies them into memory which forms a snapshot of the environment.
These values do not change throughout the rest of the cycle. Input phase takes the same time in
each scan cycle.

\item \textbf{Calculation phase} during which the PLC system
executes the instructions and writes back the results into memory. At the beginning of each
calculation phase, PLC system does some preparations, such as self-check and timer instructions
(for the timers whose base is 10ms). The preparations take the same time.

\item \textbf{Output phase} during which PLC maps
the results into actuators. Output phase takes the same time in each scan cycle.

\end{enumerate}

There are five standard programming languages for PLC \cite{IEEC61131-3} among which the Ladder
Diagram (LD) is the most widely used programming language. From now on, we concentrate on the LD
language.

As an embedded system, the real-time aspect of PLC system is ensured by the use of timers.
\footnote{Since there are many different kinds of PLCs in the industry and the instructions used in
these PLCs are different from each other, in order to ease the discussion, from now on, we focus on
S7-200 which is a kind of PLC produced by the Siemens company. In some cases, time is ensured by
the use of interruptions. We do not consider this case here.} There are mainly three kinds of
timers in S7-200\cite{s7-200-manual}: TON-timer, TONR-timer, and TOF-timer. In this paper, we focus
on the TON-timers. The other two kinds of timers can be treated in a similar manner. According to
the user manual of S7-200, a TON-timer and its behavior are demonstrated in Fig.\ref{ton_timer}. A
TON-timer has two input ports: IN that indicates whether the timer is enabled and PT that is the
preset value of the timer. There are two output ports: one for the current value and the other for
the timer bit. The characteristics of a TON-timer are informally described as follows:

\begin{enumerate}

\item A TON-timer counts time (i.e. increase its current value)
when its IN is ON and it is updated.

\item A TON-timer's timer bit is OFF and
its current value is cleared when its IN is OFF.

\item If a TON-timer's current value is greater than or equal to
its PT, its timer bit is ON.

\item A TON-timer continues counting after its PT is reached,
and stops counting when the maximum value 32767 is reached.

\end{enumerate}
A TON-timer has three resolutions: 1ms, 10ms, and 100ms. The behaviors of timers with different
resolutions are different. For the timer with time base of 1ms, it updates every 1ms asynchronously
to the scan cycle. In other words, the timer bit can be updated multiple times during one scan
cycle. For the 10ms timer, it only updates at the beginning of each scan cycle. For the 100ms
timer, its current value is updated only when the instruction is executed. The user manual
emphasizes that, for the 100ms timer, its instruction should be executed one and only one time
during each cycle.

In section \ref{model_time}, we propose a set of axioms to model the behavior of a TON-timer. This
axiom set appears sufficient for proving many properties of practical interests.

\begin{figure}[]
        \center\includegraphics[scale = 0.6]
        {figs/ton_timer}
        \caption{\label{ton_timer} TON timer and its behivour}
      \end{figure}



\section{An Illustrative Example}
\label{example}

In this section, we show a quiz machine problem as an illustrative example to explain some basic
notions of LD language, control flow graph of program, and the modeling process of TON-timers.

A quiz machine is an equipment used in a contest which involves a host and several players. The
host uses his buttons to start and reset a contest. Every player controls his button which is
associated with a light. The button is used for the player to vie to answer and the light is used
to indicate that the corresponding player has the chance to answer. After the host starts a
contest, the first player who presses his button will turn on an associated light. If more than one
players press the buttons at the same time, the machine should inform the host to restart another
contest. If during the predefined time there is no one pressing the button, the machine should
inform the host that time is out and keep all players' lights off even if some of them press their
buttons. The ladder diagram implementation of quiz machine with three players and a predefined time
of 3 seconds are shown in Fig.\ref{quizmachine}.

As shown in Fig.\ref{quizmachine}, a LD program consists of a set of rungs. There are 10 rungs in
the example program. Each rung can be seen as a connection between logical checkers (contacts or
relays) and actuators (coils). For example, the first rung contains three relays (i.e. $m_1$, $i_1$
and $i_0$) and one coil (i.e. $m_1$). Normally, each rung has only one coil. If a path can be
traced between the left side of the rung and the coil, through ON contacts, the rung is true and
the output coil storage bit is ON. A normally open contact (-$|~|$-) is closed (ON) when its bit is
1 and it is normally OFF. A normally closed contact (-$|/|$-) is closed (ON) when its coil is 0 and
it is normally ON.

In the program, $m_1$ is used to indicate whether the contest begins. $m_2$, $m_3$, and $m_4$
denote whether play$_1$, play$_2$, or play$_3$ presses his button, respectively. TON-timer $t_1$ is
used to record whether the time after the host presses start button is longer than the predefined
time. $m_5$ represents whether there is a player that presses his button. $o_1$, $o_2$, and $o_3$
are used to turn on the corresponding lights $l_1$, $l_2$, and $l_3$, respectively. $o_0$ denotes
whether the time is out.

Three time related program properties should be satisfied. The host presses the reset button and,
after a while, he presses the start button. Between the time he presses the start button and the
timeout:

\begin{itemize}

\item if there is only one who first press his button,
the corresponding light will turn on and the other lights stay off;

\item if at least two players first press their buttons at the same,
their lights will be turned on and the other lights stay off;

\item if no one presses the button, the light indicating timeout will turn on and the other lights stay off.

\end{itemize}

\begin{figure}[]
        \center\includegraphics[scale = 0.45]
        {figs/quizmachine}
        \caption{\label{quizmachine} The Ladder Diagram of Quiz Mechine}
      \end{figure}


\section{Modeling PLC Programs with Timers}
\label{model_timer}

Following the criteria proposed in \cite{Mader00aclassification}, we show our method of modeling
PLC programs with timers in three steps:
\begin{enumerate}

\item programming language fragments that are used and
assumptions and constraints of the PLC programs;

\item to what extent and how the cyclic operation mode is modeled;

\item how to model the timer.

\end{enumerate}
We first introduce the control flow graph and its associated table which give us a formal base for
the sequent discussions.

\subsection{Control Flow Graph of PLC Programs}
\label{abstract_structure}

The structure of a PLC program can be described by a control flow graph (CFG). As an example, the
CFG of the quiz program is shown in Fig.\ref{cfg_quiz_mechine}. Node $0$ represents the preparation
at the beginning of the calculation phase. Each of the rest nodes denotes a rung in the program.
Since there is no loop and case constructs in the program, the CFG is a simple straight line. Every
node $i$ is associated with three sets:  $ref_i$, $def_i$, and $times_i$, where $ref_i$ is the set
of variables node $i$ refers to, $def_i$ is the set of variables node $i$ defines and $times_i$ is
the set of all possible time spans used to reach node $i$ from the beginning of the calculation
phase. Tab.\ref{tab_ref_def} shows the sets for each node. The superscript $i$ of each variable in
the $ref_i$ means the variable is defined at node $i$. For instance, $m^1_1$ in $ref_2$ means $m_1$
used at node $2$ is defined at node $1$. We assume the executions of each rung cost the same time
which is 3ms.\footnote{The execution times for different rungs can be different, but this doesn't
effect the modeling and verification process.} CFG and the table form a formal representation of a
PLC program's structure.

Timer bits are special variables in PLC. Comparing to other variables, their values can change
multiple times without explicit assignments. If 1ms TON-timer is chosen for the program in
Fig.\ref{quizmachine}, we need to add $t_1$ to every $ref_i$ -- since it can update asynchronously
to the scan cycle --  and make some modifications to $t^*_1$ in each $ref_i$. The result table is
shown in Tab.\ref{tab_ref_def_1ms}.

\begin{figure}[]
        \center\includegraphics[scale = 0.66]
        {figs/cfg_quiz_mechine}
        \caption{\label{cfg_quiz_mechine} The CFG of the quiz machine program}
      \end{figure}


\begin{table}
 \caption{\label{tab_ref_def} $ref$s and $def$s for the CFG of quiz machine}
\begin{center}
\begin{tabular}{c| c| c |c }
\hline Node No. & $ref$ & $def$ & $times$\\

\hline
0 & \{$$\} & \{$$\} & \{0ms\}\\
1 & \{$i_0,i_1,m^1_1$\} & \{$m_1$\} & \{3ms\}\\
2 & \{$m^1_1$\} & \{$t_1$\}  & \{6ms\}\\
3 & \{$t^2_1,i_2,m^6_5,m^1_1,m^3_2$\} & \{$m_2$\}  & \{9ms\}\\
4 & \{$t^2_1,i_3,m^6_5,m^1_1,m^4_3$\} & \{$m_3$\}  & \{12ms\}\\
5 & \{$t^2_1,i_4,m^6_5,m^1_1,m^5_4$\} & \{$m_4$\}  & \{15ms\}\\
6 & \{$m^1_1,m^3_2,m^4_3,m^5_4,m^6_5$\} & \{$m_5$\}  & \{18ms\}\\
7 & \{$m^3_2$\} & \{$o_1$\}  & \{21ms\}\\
8 & \{$m^4_3$\} & \{$o_2$\}  & \{24ms\}\\
9 & \{$m^5_4$\} & \{$o_3$\}  & \{27ms\}\\
10 & \{$t^2_1,m^6_5$\} & \{$o_0$\}  & \{30ms\}\\
\hline

\end{tabular}
\end{center}
\end{table}

\begin{table}
 \caption{\label{tab_ref_def_1ms}$ref$s and $def$s for the CFG of quiz machine with 1ms TON-timer}
\begin{center}
\begin{tabular}{c| c| c |c}
\hline Node No. & $ref$ & $def$ & $times$\\

\hline
0 & \{$$\} & \{$t_1$\} & \{0ms\} \\
1 & \{$i_0,i_1,m^1_1$\} & \{$m_1,t_1$\} & \{3ms\} \\
2 & \{$m^1_1$\} & \{$t_1$\}& \{6ms\}\\
3 & \{$t^2_1,i_2,m^6_5,m^1_1,m^3_2$\} & \{$m_2,t_1$\}  & \{9ms\}\\
4 & \{$t^3_1,i_3,m^6_5,m^1_1,m^4_3$\} & \{$m_3,t_1$\}  & \{12ms\}\\
5 & \{$t^4_1,i_4,m^6_5,m^1_1,m^5_4$\} & \{$m_4,t_1$\}  & \{15ms\}\\
6 & \{$m^1_1,m^3_2,m^4_3,m^5_4,m^6_5$\} & \{$m_5,t_1$\}  & \{18ms\}\\
7 & \{$m^3_2$\} & \{$o_1,t_1$\}  & \{21ms\}\\
8 & \{$m^4_3$\} & \{$o_2,t_1$\}  & \{24ms\}\\
9 & \{$m^5_4$\} & \{$o_3,t_1$\}  & \{27ms\}\\
10 & \{$t^9_1,m^6_5$\} & \{$o_0,t_1$\}  & \{30ms\}\\
\hline

\end{tabular}
\end{center}
\end{table}



\subsection{Assumptions and Constraints}
\label{assumption_constraits}

We articulate the assumptions and constraints below and explain how to modify the programs that did
not meet these properties to make them satisfy these properties:

\begin{enumerate}

\item The executions of the same instruction take the same time.

\item There is no loop, i.e. the corresponding CFG is an acyclic graph.

\item There is no cross reference among timer instructions,
i.e. a timer cannot use another timer's timer bit or current value to calculate its IN point.

\item During one scan cycle, the values of a TON-timer used
by several instructions are the same.
 This can be stated formally as $\forall n_1~
n_2~n_3~n_4:Nodes~ t:Timers, t^{n_3}\in ref_{n_1} \vee t^{n4}\in ref_{n_2} \rightarrow n_3 = n_4$.
If the program does not satisfy the constraint, this could cause unfair treatment to players in the
quiz contest. Given a program does not satisfy the constraint, the following modifications should
be made to the program:

\begin{itemize}

\item \textbf{1ms TON-timer.} For each 1ms TON-timer $t$,
a new variable $m$ is introduced and a new rung ``${|--|~t~|--(m)}$'' is inserted before the first
reference to $t$. All the references to $t$ are replace by the references of $m$. For example, if
1ms TON-timer is used in the program shown in Fig.\ref{quizmachine}, the program does not satisfy
this constraint for the values used at node 3 and 4 are different i.e. in Tab.\ref{tab_ref_def_1ms}
the superscripts of $t_1$ at nodes 3 and 4 are different. The table of the program after
modification is shown in Tab.\ref{tab_ref_def_1ms_mod} from which it can be verified that the
program holds the constraint.

\begin{table}
 \caption{\label{tab_ref_def_1ms_mod}$ref$s and $def$s for the CFG of modified quiz machine with 1ms TON-timer}
\begin{center}
\begin{tabular}{c| c| c |c}
\hline Node No. & $ref$ & $def$ & $times$\\

\hline
0 & \{$$\} & \{$t_1$\} & \{0ms\} \\
1 & \{$i_0,i_1,m^1_1$\} & \{$m_1,t_1$\} & \{3ms\} \\
2 & \{$m^1_1$\} & \{$t_1$\}& \{6ms\}\\
3 & \{$t^2_1$\} & \{$m_6$\}  & \{9ms\}\\
4 & \{$m^3_6,i_2,m^6_5,m^1_1,m^3_2$\} & \{$m_2,t_1$\}  & \{12ms\}\\
5 & \{$m^3_6,i_3,m^6_5,m^1_1,m^4_3$\} & \{$m_3,t_1$\}  & \{15ms\}\\
6 & \{$m^3_6,i_4,m^6_5,m^1_1,m^5_4$\} & \{$m_4,t_1$\}  & \{18ms\}\\
7 & \{$m^1_1,m^3_2,m^4_3,m^5_4,m^6_5$\} & \{$m_5,t_1$\}  & \{21ms\}\\
8 & \{$m^3_2$\} & \{$o_1,t_1$\}  & \{24ms\}\\
9 & \{$m^4_3$\} & \{$o_2,t_1$\}  & \{27ms\}\\
10 & \{$m^5_4$\} & \{$o_3,t_1$\}  & \{30ms\}\\
11 & \{$m^3_6,m^6_5$\} & \{$o_0,t_1$\}  & \{33ms\}\\
\hline

\end{tabular}
\end{center}
\end{table}

\item \textbf{10ms and 100ms TON-timers.} No modification is needed.

\end{itemize}

\item For each node $i$ in CFG  that defines a timer, i.e. the timer is in $def_i$, and
referred by other nodes in the same cycle, the cardinality of $times_i$ is 1. In other words, for
such node there is one and only one path to reach it.

\item Each relay can be set value at most once per scan cycle.
Modifications described in \cite{SynSignalModelPLC} can be made to programs that do not satisfy
this constraint.

\end{enumerate}

It can be verified that the program corresponding to Tab.\ref{tab_ref_def} and
Tab.\ref{tab_ref_def_1ms_mod}
 satisfy all the above constraints. We will discuss the reason why we have
these assumptions and constraints in the following sections.

\subsection{Cyclic Behavior, Relays and Time}
\label{scan_cycle_relay}

According to \cite{Mader00aclassification}, there are four ways to model scan cycle: models without
scan cycle, models with explicit scan cycle, models with implicit scan cycle, and models abstracted
from scan cycle. Our model belongs to the third kind.

Models with implicit scan cycle can be simply understood as the modeling of cyclical behavior, but
the duration of each scan cycle is not considered. The reasons why we chose this are as follows:

\begin{itemize}

\item In practice, the duration of each scan cycle and the
execution time of each instruction are not of great importance. What we concern is only the
summation of durations of several adjacent scan cycles.

\item We want to get a simpler model. If we take into account the execution time of each
instruction, several auxiliary notations need to be added into the model. Though it could make our
model more precise, it makes the model more complex and the reasoning more difficult which is not
necessary.

\end{itemize}

In PLC, relays are used to store input values, internal values and output values. The modeling of
scan cycle is represented by the modeling of relays. We define a variable $Cycle$ as the total
number of scan cycles from the start of the program. {\small
\begin{verbatim}
Definition Cycle := nat.
\end{verbatim}
} After the definition of scan cycle, there are three things to do: 1) define the value of each
relay at each scan cycle; 2) attach time to each scan cycle; 3) determine the interpretation
location of the value and time for each scan cycle.

\subsubsection{Values of Relays} The values (i.e. ON and OFF) of relays
change according to the cycles. In other words, they are functions from $Cycle$ to Boolean: {\small
\begin{verbatim}
Definition Var := Cycle -> bool.
\end{verbatim}
} Since Coq  is a system based on intuitive logic, the results of logic computation are in the sort
$Prop$. In order to facilitate the proof process, we use the following definition instead: {\small
\begin{verbatim}
Definition Var := Cycle -> Prop.
\end{verbatim}
} For example, given a relay $r$ of type $Var$ and a cycle $i$, $r(pred ~i)$ and $(r~i)$ are used
to denote the values of relay $r$ at cycle ($i-1$) and cycle $i$, respectively.

\subsubsection{Time}Time is defined by natural number:
{\small
\begin{verbatim}
Definition Time := nat.
\end{verbatim}
}  Function $f$ associates each scan cycle with a time: {\small
\begin{verbatim}
Variable f : Cycle -> Time.
\end{verbatim}
} Function $f$ should satisfy the monotonic property which means that the time attached to scan
cycles increases strictly: {\small
\begin{verbatim}
Hypothesis f_monotonic:forall c, f c < f (S c).
\end{verbatim}
}
\subsubsection{Interpretations of Values and Times}

The value of a relay and time at a cycle can have several interpretations. For instance, given a
relay $r$, the values of $r$ along the execution of PLC program form an infinite trace which is
illustrated in Fig.\ref{interpretatino_of_cycle}. This trace alternates the I/O phase and
calculation phase infinitely. The inner values of $r$ during the calculation phase is not of
concern here. Intuitively, in Fig.\ref{interpretatino_of_cycle} the first point represents the
value of $r$ at the beginning of the I/O phase of cycle $0$, the second point represents the value
of $r$ at the beginning of the calculation phase of cycle $0$, and so on. Thus, $(r~0)$ can have at
least three different interpretations depending on whether the value is sampled at $a$, $b$ or $c$.
If $b$ is chosen, abstract trace $A$ is extracted from the concrete trace. In case of $c$, abstract
trace $B$ is obtained. An abstract trace is a division of the concrete trace. Different abstract
traces separate the I/O phases and calculation phases differently. For trace $B$, an I/O phase and
its following calculation phase belong to the same abstract cycle which is similar to the standard
understanding of scan cycle. For trace $A$, a calculation phase and its following I/O phase belong
to the same abstract cycle. Based on different abstract trace, different abstract models can be
obtained. For example, two models can be built for the first rung in Fig.\ref{quizmachine}: {\small
\begin{verbatim}
% abstract model A
Variables i0 i1 m1 : Var.
Hypothesis h_m1 : forall c, m1 c =
  ((i0 (pred c)\/m1 (pred c))/\~i1 (pred c)).
% abstract model B
Variables i0 i1 m1 : Var.
Hypothesis h_m1 : forall c, m1 c =
  ((i0 c \/ m1 (pred c)) /\ ~ i1 c).
\end{verbatim}
} In the first model, since the calculation of $m_1$'s value at cycle $c$ is based on the values of
$i_0$ and $i_1$ at the previous cycle, $i_0~(pred~c)$ and $i_1~(pred~c)$ are used. In the second
model, the calculation of $m_1$ uses the values of $i_0$ and $i_1$ at the current cycle, so $i_0~c$
and $i_1~c$ are used.

The discussion about the interpretations of time is similar to that of relay values. This will be
discussed in detail in section \ref{model_time}.

\begin{figure}[]
        \center\includegraphics[scale = 0.5]
        {figs/interpretatino_of_cycle}
        \caption{\label{interpretatino_of_cycle} Different interpretations of value at a cycle}
      \end{figure}


\subsection{Rungs and Their Execution Order}

Every rung is modeled by a hypothesis in Coq. The execution order of instructions in a PLC program
should be reflected by the model. According to the cyclic behavior of PLC and the execution order
of instructions, for each node $i$, its $ref_i$ can be divided into two disjoint subsets: $ref^c_i$
and $ref^p_i$, where $ref^c_i$ stands for the set of variables whose values at the current scan
cycle are used for the execution of $i$ and $ref^p_i$ stands for the set of variables whose values
of the previous scan cycle are used for the execution of $i$. Let us take the sixth rung in
Fig.\ref{quizmachine} for example, $ref^c_6=\{m_1,m_2,m_3,m_4\}$ and $ref^p_6=\{m_5\}$. For any
cycle $c$, $v^c \in ref^c_6$ and $v^p \in ref^p_6$, $(v^c~c)$ and $(v^p~(pred~c))$ are used to
calculate $m_5$. Hence, we have the following Coq codes for the sixth rung: {\small
\begin{verbatim}
Hypothesis h_m5 : forall c, m5 c =
  (((m2 c\/m3 c\/m4 c)\/m5 (pred c))/\m1 c).
\end{verbatim}
}
\subsection{TON-Timer}
\label{model_time}

As mentioned in section \ref{scan_cycle_relay}, based on different abstractions we have different
models for TON-timers. We first give the assumption about the preset time of $t_1$, then choose an
interpretation location, finally build a model for $t_1$.

\subsubsection{Assumptions about Time}

Based on the above notations, definitions of timer bit and preset time of the TON-timer are given
as follows ($t_1$ is used to denote the timer bit and $t_1\_PT$ of type $Time$ denotes the preset
time): {\small
\begin{verbatim}
Variable t1:Var. Variable t1_PT:Time.
\end{verbatim}
} In practice, the preset time of $t_1$ must be greater than time span of any adjacent scan cycles:
{\small
\begin{verbatim}
Hypothesis f_TLTCI :
  forall c, f (S c) -  f c < t1_PT.
\end{verbatim}
}

\subsubsection{The Interpretation Location}
\label{interpretation_loc}

The concrete trace of quiz machine is shown in Fig.\ref{traces_simple_example_2}. We concern the
inner values in the calculation phase here. We have several different interpretation locations.
Here we choose location $a$. The abstract trace is the line below. The model of TON-timer $t_1$ is
represented by three axioms: {\small
\begin{verbatim}
Axiom h_t1_reset : forall c, ~ m1 c -> ~ t1 c.
Axiom h_t1_set :
  forall c1 c2, t1_PT<=f(pred c2)-f(pred c1)->
    being_true m1 c1 c2 -> t1 c2.
Axiom h_t1_true :
  forall c2, t1 c2->exists c1,
    t1_PT<=f(pred c2) - f (pred c1) /\
    being_true m1 c1 c2.
\end{verbatim}
}

\begin{figure*}[]
        \center\includegraphics[scale = 0.88]
        {figs/traces_simple_example_2}
        \caption{\label{traces_simple_example_2} Concrete and abstract traces}
      \end{figure*}

Axiom $h\_t1\_reset$ reflects the second characteristic of TON-timer. The references to the same
cycle $c$ in ``$m_1~c$'' and ``$t_1~c$'' show the fact that the value of $m_1$ affects the value of
$t_1$ in the same cycle. The meaning of the second axiom can be explained using
Fig.\ref{traces_simple_example_2}. Suppose in the abstract trace the time span from $(pred~ c_1)$
to $(pred ~c_2)$ is greater than or equal to $t_1\_PT$ (which is presented by
``$t_1\_PT<=f~(pred~c_2)~-~f~(pred~c_1)$'') and $m_1$ is ON between $c_1$ and $c_2$ (which is
expressed by the predicate ``$being\_true ~m_1 ~c_1~c_2$''). Hence in the concrete trace the time
span between $a$ and $e$ is greater than or equal to $t_1\_PT$. Because of the fifth constraint
mentioned in section \ref{assumption_constraits}, the time span between $a$ and $b$ is equal to the
time span between $e$ and $f$. Finally we have that the time span between $b$ and $f$ is greater
than or equal to $t_1\_PT$. Note that $rung_2$ contains the timer instruction. Together with the
fact that $m_1$ stays ON from $b$ to $g$, we have that $t_1$ is ON at $g$ in the concrete trace, in
other words $t_1$ is ON at cycle $c2$ in the abstract trace, which is the conclusion of the second
axiom. The third axiom can be understood in a similar manner.

These axioms forms a parameterized module for a TON-timer. The module has two parameters: $IN$
(which is $m_1$ in the example) and $PT$ (which is $t_1\_PT$ in the example).

In general, the statement of these hypothesis have to be universally quantified over arbitrary
inputs and outputs. For the convenience of this study, we assume that the hypothesis have been
instantiated by the concrete variables in the program.

\section{The Complete Model of Quiz Machine}
\label{whold_model}

The complete model of the quiz program is shown below:

{\small
\begin{verbatim}
Variables i0 i1 i2 i3 i4 : Var.
Variables m1 m2 m3 m4 m5: Var.
Variables o0 o1 o2 o3 : Var.

Variable t1 : Var.
Variables t1_PT : Time.
Hypothesis f_TLTCI :
  forall c, f (S c) -  f c < t1_PT.
Axiom h_t1_reset : forall c, ~ m1 c -> ~ t1 c.
Axiom h_t1_set :
  forall c1 c2, t1_PT<=f(pred c2)-f(pred c1)->
    being_true m1 c1 c2 -> t1 c2.
Axiom h_t1_true :
  forall c2, t1 c2->exists c1,
    t1_PT<=f(pred c2) - f (pred c1) /\
    being_true m1 c1 c2.

Hypothesis h_m1 : forall c, m1 c =
  ((i0 c \/ m1 (pred c)) /\ ~ i1 c).
Hypothesis h_m2 : forall c, m2 c =
  (((~ t1 c /\ i2 c /\ ~ m5 (pred c))
  \/ m2 (pred c)) /\ m1 c).
Hypothesis h_m3 : forall c, m3 c =
  (((~ t1 c /\ i3 c /\ ~ m5 (pred c))
  \/ m3 (pred c)) /\ m1 c).
Hypothesis h_m4 : forall c, m4 c =
  (((~ t1 c /\ i4 c /\ ~ m5 (pred c))
  \/ m4 (pred c)) /\ m1 c).
Hypothesis h_m5 : forall c, m5 c =
  (((m2 c \/ m3 c \/ m4 c) \/
  m5 (pred c)) /\ m1 c).
Hypothesis h_o1 : forall c, o1 c = m2 c.
Hypothesis h_o2 : forall c, o2 c = m3 c.
Hypothesis h_o3 : forall c, o3 c = m4 c.
Hypothesis h_o0 : forall c, o0 c=(t1 c/\~m5 c).
\end{verbatim}
}

The above model can be understood as a module with one parameter ``$t_1\_PT$'' and a property
``$f\_TLTCI$'' that the parameter should satisfy. By giving ``$t_1\_PT$'' a constant that satisfies
``$f\_TLTCI$'' to the module, an instance can be obtained such that all properties the
parameterized module hold are also held by the instance.

\subsection{Formalization of Properties}

We proved that three expected behaviors, each of which is described in a theorem, hold in Coq. The
first of these properties is delineated in the following theorem. It describes the situation that
one player presses his button and then the associated light is turned on. The theorem contains
various conditions to make sure that the action can proceed. In order to make the theorem clear,
several predicates, such as $reset\_then\_start$ and $just\_time\_out$, are introduced. They will
be explained along the description of the theorem.

%\begin{itemize}

%\item
{\small
\begin{verbatim}
Theorem reset_start_time_i2_o0o1o2o3_f :
  forall c1 c2, reset_then_start c1 c2 ->
    forall c3, just_time_out c2 c3 ->
     forall c, S c2 <= c <= c3 ->
       p1_first_presses (S c2) c ->
         forall c4, c <= c4 ->
           not_reset (S c2) c4 ->
           stay_off o0 (S c2) c4 /\
           off_on o1 (S c2) c c4 /\
           stay_off o2 (S c2) c4 /\
           stay_off o3 (S c2) c4.
\end{verbatim}
}
%\item
%\begin{verbatim}
%Theorem reset_start_time_i2i3_o0o1o2o3_f :
%    forall c1 c2, reset_then_start c1 c2 ->
%        forall c3,
%            just_time_out (S c2) c3 ->
%            forall c,
%            S c2 <= c <= c3 ->
%            p1p2_first_press (S c2) c ->
%            forall c4, c <= c4 ->
%                not_reset (S c2) c4 ->
%                stay_off o0 (S c2) c4 /\
%                off_on o1 (S c2) c c4 /\
%                off_on o2 (S c2) c c4 /\
%                stay_off o3 (S c2) c4.
%\end{verbatim}

%\item
%\begin{verbatim}
%Theorem reset_start_exceed_time_o0o1o2o3_f :
%    forall c1 c2, reset_then_start c1 c2 ->
%        forall c3,
%            just_time_out (S c2) c3 ->
%            no_player_press (S c2) c3 ->
%            forall c4, S c3 <= c4 ->
%                not_reset (S c2) c4 ->
%                off_on o0 (S c2) (S c3) c4 /\
%                stay_off o1 (S c2) c4 /\
%                stay_off o2 (S c2) c4 /\
%                stay_off o3 (S c2) c4.
%\end{verbatim}

%\end{itemize}

The formulae before the last arrow present the premises, i.e. the behaviors of the environment
(including the actions of the host and players); those after the last arrow describe the
conclusions, i.e. the expected behavior of the system. Fig.\ref{fig_theorem_1} is a graphic
representation of the theorem, where the words above the horizontal arrow describe the premises and
the words below the arrow describe the conclusions. Predicate ``$reset\_then\_start ~c_1 ~c_2$''
expresses the action sequence of the host: the host presses reset button at cycle $c_1$ and does
not press start button from cycle $c_1$ to cycle $c_2$, then he presses start button at cycle $(S
~c_2)$ (i.e. the next cycle of $c_2$). Predicate ``$just\_time\_out ~c_2~ c_3$'' means the time
span between $c_2$ and $c_3$ is less than $t_1\_PT$ and that between $c_2$ and $(S ~c_3)$ is equal
or larger than $t_1\_PT$. Predicate ``$p1\_first\_presses~ (S~ c_2)~ c$'' describes the fact that
there exists a cycle $c$ such that between $(S~ c_2)$ and $(pred ~c)$ no one presses his button and
at $c$ player$_1$ is the only one that presses his button. Predicate ``$not\_reset~ (S~ c_2)~
c_4$'' means during $(S~c_2)$ and $c_4$ the reset button is not pressed. The conclusion has four
predicates: 1) ``$off\_on~ o_1~ (S~ c_2)~ c~ c_4$'' means that light$_1$ is off between $S~c_2$ and
$pred~c$ and light$_1$ is on between $c$ and $c_4$; 2) ``$stay\_off~ o_0 ~(S~ c_2)~ c_4$'',
``$stay\_off ~o_2 ~(S~c_2) ~c_4$'' and ``$stay\_off ~o_2 (S~ c_2) ~c_4$'' describe that between $S
~c_2$ and $c_4$ light$_0$, light$_1$ and light$_3$ are all off.


\begin{figure}[]
        \includegraphics[scale = 0.50]
        {figs/fig_theorem_1}
        \caption{\label{fig_theorem_1}Graphic representation of theorem 1}
      \end{figure}

\subsection{Outline of the Proof}

Since the proofs of the three theorems are lengthy -- the whole file has more than two thousand
lines -- we only outline the proof skeleton here.

The model of the quiz machine can be considered as a transition system. The state of the system is
an vector consisting of all the internal relays : ($m_1,m_2,m_3,m_4,m_5$). The inputs of the
program (i.e. $i_0,i_1,i_2,i_3$ and $i_4$) and the timeout signal (i.e. $t_1$) are the guards on
the transitions. Part of transition system used to prove the theorem is demonstrated in
Fig.\ref{fig_quizm_trans}. The numbers in the states above the line indicate the values of
$m_1,m_2,m_3$ and $m_5$ respectively and those below the line indicate the values of $o_0,o_1,o_2$
and $o_3$. The variables above the transitions represent the conditions under which the
corresponding transition can take place. Variables not mentioned means the transition does not care
the values of these variables. For instance, if the system is at state $s_1$, then all the output
and internal relays are $0$. If $i_0$ is false, whatever values the other variables are the system
stays in $s_1$. If $i_0$ is true, the system will change to state $s_2$.

The promises of the theorem express the inputs of the system and their orders:

\begin{enumerate}

\item The host presses the reset button.

\item The host presses the start button and does not press the reset button afterwards.

\item Player$_1$ firstly presses his button before the timeout.

\end{enumerate}
We proved that following the above inputs the system
\begin{enumerate}

\item reaches $s_1$ after the host presses the reset button; then

\item it reaches $s_2$ after the host presses the start button; then

\item it reaches $s_3$ after player$_1$ presses his button before
timeout.
\end{enumerate}
And the outputs of this process coincide with the conclusion of the theorem. The other two theorems
are proved in the same manner.


\begin{figure}[]
        \includegraphics[scale = 0.5]
        {figs/QuizMachine_transition}
        \caption{\label{fig_quizm_trans}Part of the transition system}
      \end{figure}

\section{Conclusions}
\label{conclusion}

We presented a formalization of the TON timer of programmable logic controllers (PLCs) in the
theorem prover Coq. In order to ease the modeling and verification process a sound abstract model
is proposed. Based on different interpretations, different abstract models can be obtained. The
behavior of the TON-timer is described by a set of axioms at an abstract level, which proves to be
appropriate for the formal reasoning in this paper. A quiz machine program with TON-timer is
employed as an illustration example throughout the paper. We proved that the PLC quiz machine
program works as expected. This work demonstrates the complexity of formal timer modeling.


\begin{thebibliography}{10}

\bibitem{Mader99timedautomaton}
Mader, A., Wupper, H.:
\newblock Timed automaton models for simple programmable logic controllers.
\newblock In: Proceedings of the Euromicro Conference on Real-Time Systems,
  IEEE Computer Society (1999)  114--122

\bibitem{ProvingSequentialFunctionChartProgramsUsingAutomata}
L'Her, D., Parc, P.L., Marc\'{e}, L.:
\newblock Proving sequential function chart programs using automata.
\newblock In: WIA '98: Revised Papers from the Third International Workshop on
  Automata Implementation, London, UK, Springer-Verlag (1999)  149--163

\bibitem{dierks01plcautomata}
Dierks, H.:
\newblock {PLC}-automata: a new class of implementable real-time automata.
\newblock Theoretical Computer Science \textbf{253}(1) (2001)  61--93

\bibitem{NBauer:Thesis:1998}
Bauer, N.:
\newblock \"ubersetzung von steuerungsprogrammen in formale modelle.
\newblock Master's thesis, University of Dortmund (1998)

\bibitem{ModellingPLCLV}
Moon, I.:
\newblock Modelling programmable logic controllers for logic verification.
\newblock IEEE Control Systems Magazine \textbf{14}(2) (1994)  53--59

\bibitem{DBLP:journals/rts/KramerV97}
Kr{\"a}mer, B.J., V{\"o}lker, N.:
\newblock A highly dependable computing architecture for safety-critical
  control applications.
\newblock Real-Time Systems \textbf{13}(3) (1997)  237--251

\bibitem{SynSignalModelPLC}
Jim\'{e}nez-Fraustro, F., Rutten, E.:
\newblock A synchronous model of iec 61131 {PLC} languages in signal.
\newblock In: ECRTS '01: Proceedings of the 13th Euromicro Conference on
  Real-Time Systems, Washington, DC, USA, IEEE Computer Society (2001)  135

\bibitem{IEEC61131-3}
{IEC International Standard 1131-3}:
\newblock Programmable Controllers, Part 3: Programming Languages.
\newblock (1993)

\bibitem{s7-200-manual}
{Siemens}:
\newblock S7-200 Programmable Controller System Manual.
\newblock Siemens (2003)

\bibitem{Mader00aclassification}
Mader, A.:
\newblock A classification of {PLC} models and applications.
\newblock In: In WODES 2000: 5th Workshop on Discrete Event Systems, Kluwer
  Academic Publishers (2000)  21--23

\end{thebibliography}

\end{document}
